$\forall$$A$, $B$:Type, ${\it eq}_{1}$:EqDecider($A$), ${\it eq}_{2}$:EqDecider($B$), $L$:((:$A$ $\times$ $B$) List).
\\[0ex]no\_repeats($A$;fpf{-}domain(fpf($L$)))
\\[0ex]\& ($\forall$$a$:$A$. ($a$ $\in$ fpf{-}domain(fpf($L$))) $\Leftarrow\!\Rightarrow$ ($\exists$$b$:$B$. ($<$$a$, $b$$>$ $\in$ $L$)))
\\[0ex]\& $\forall$$a$$\in$dom(fpf($L$)). $l$=fpf($L$)($a$) $\Rightarrow$  no\_repeats($B$;$l$) \& ($\forall$$b$:$B$. ($b$ $\in$ $l$) $\Leftarrow\!\Rightarrow$ ($<$$a$, $b$$>$ $\in$ $L$))